Sequent calculus

⊢ ( turnstile ) の前後に命題を並べる。

左の命題がすべて成り立っている場合は、右の命題のどれかが成り立つ、と読む

左の命題が空で、右の命題が1つの場合に、その命題は定理と呼ばれる。(前提なしに成り立つ文なので)

推論ルール

1 ID

2 CUT

3 AND L1

4 OR R1

5 AND L2

6 OR R2

7 OR L

8 AND R

9 IMPLY L

10 IMPLY R

11 NOT L

12 NOT R

13 FOR ALL L

14 FOR ALL R

15 EXIST L

16 EXIST R

17 WL

18 WR

19 CL

20 CR

21 PL

22 PR

実装プラン